<html>
<head><meta charset="utf-8"><title>Emulation of SIMD for verification · project-portable-simd · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/index.html">project-portable-simd</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html">Emulation of SIMD for verification</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="238923067"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238923067" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238923067">(May 15 2021 at 20:24)</a>:</h4>
<p>This is interesting: it looks like there's movement towards emulation of vectorized code. <a href="https://project-oak.github.io/rust-verification-tools/2021/05/15/verifying-vectorized-code2.html">https://project-oak.github.io/rust-verification-tools/2021/05/15/verifying-vectorized-code2.html</a></p>



<a name="238926878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238926878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238926878">(May 15 2021 at 21:32)</a>:</h4>
<p>The emulation library is here: <a href="https://github.com/project-oak/rust-verification-tools/tree/main/simd_emulation">https://github.com/project-oak/rust-verification-tools/tree/main/simd_emulation</a><br>
Currently x86 only, only supports the architecture specific instructions that I see in LLVM IR when I compile programs.<br>
I wrote it to support formal verification with one particular verifier (KLEE) but my goal is that it should be usable by any verifier whether LLVM-based or MIR-based or by miri or, indeed, by anything that needs to know  the semantics of a SIMD instruction.</p>
<p>To do this, more instructions, architectures, etc. will need to be added; we'll need a plan for testing the library (it is basically untested at present); etc.<br>
I'm happy to work with other potential users to get there.</p>



<a name="238929285"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238929285" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238929285">(May 15 2021 at 22:17)</a>:</h4>
<p>Interesting. This looks a lot like what we'll have to do for the Cranelift-friendly-intrinsics plan, and is definitely similar to what we've been doing for our own testing rigs.</p>



<a name="238929594"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238929594" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238929594">(May 15 2021 at 22:23)</a>:</h4>
<p>What's really weird is the repo is invisible from <a href="https://github.com/project-oak">https://github.com/project-oak</a></p>



<a name="238929768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238929768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238929768">(May 15 2021 at 22:26)</a>:</h4>
<p>Okay, so you're operating on the bitcode, examining that, finding the LLVM signature for a given x86 assembly instruction or intrinsic, and then executing a function based on that.</p>



<a name="238929936"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238929936" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238929936">(May 15 2021 at 22:30)</a>:</h4>
<p>I imagine the architecture-agnostic LLVM instructions do not need to be emulated?</p>



<a name="238930001"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930001" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930001">(May 15 2021 at 22:32)</a>:</h4>
<p>It depends on what stage Alastair is operating at. It seems to be after bitcode is constructed, which is pretty late in the game, so I think it winds up with everything being lowered to a given architecture-specific instruction set anyways?</p>



<a name="238930204"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930204" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930204">(May 15 2021 at 22:34)</a>:</h4>
<p>No, the LLVM instructions are compiled to assembly</p>



<a name="238930230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930230">(May 15 2021 at 22:35)</a>:</h4>
<p>They're the same as scalar instructions</p>



<a name="238930389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930389">(May 15 2021 at 22:38)</a>:</h4>
<p>hmmm.</p>



<a name="238930893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930893">(May 15 2021 at 22:48)</a>:</h4>
<p>I wonder if it wouldn't be easier to emulate the x86 assembly instructions directly and then map LLVM's model of the intrinsics to that.</p>



<a name="238930983"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238930983" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238930983">(May 15 2021 at 22:50)</a>:</h4>
<p>Why do LLVM's need to be emulated?</p>



<a name="238931106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931106">(May 15 2021 at 22:53)</a>:</h4>
<p>I don't think we run into this with cranelift either, because cranelift is just going to implement the intrinsics</p>



<a name="238931171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931171">(May 15 2021 at 22:54)</a>:</h4>
<p><span class="user-mention" data-user-id="281757">@Jubilee</span> Our intrinsics are a directory within a broader repo containing tools, libraries, scripts, etc to support formal verification of Rust. Making it a separate repository adds friction in various forms - so it made sense not to make it standalone right from the start. If others want to work on it, the right thing would obviously be to move that crate to a more 'central' place.</p>



<a name="238931257"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931257" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931257">(May 15 2021 at 22:56)</a>:</h4>
<p>OH I have an extension that's bugging for me, ignore that remark about repos being invisible.</p>



<a name="238931273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931273">(May 15 2021 at 22:57)</a>:</h4>
<p>Yeah with it off suddenly everything is fixed and everything I expect to see is seen! cool.</p>



<a name="238931351"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931351" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931351">(May 15 2021 at 22:59)</a>:</h4>
<p><span class="user-mention" data-user-id="312331">@Caleb Zulawski</span> For our <em>current</em> purposes, we don't need to emulate the architecture agnostic SIMD intrinsics because (as far as I can tell), LLVM is able to expand those intrinsics on demand. Specifically, we are using the KLEE symbolic execution tool and it calls an LLVM function that lowers a bunch of different LLVM intrinsics including (I believe) the agnostic SIMD intrinsics but not the x86 specific intrinsics.</p>



<a name="238931363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931363">(May 15 2021 at 22:59)</a>:</h4>
<p>Okay, cool, just confirming because we only use the agnostic ones</p>



<a name="238931425"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931425" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931425">(May 15 2021 at 23:00)</a>:</h4>
<p>Well, there's some dirty hacks in <code>cg_llvm</code>, so idk if we can rule out ever using an arch-specific one from the perspective of someone touching LLVM bitcode.</p>



<a name="238931624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Caleb Zulawski <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931624">(May 15 2021 at 23:03)</a>:</h4>
<p>Hmm I've never seen one.  But I think it should be the rule</p>



<a name="238931631"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931631" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931631">(May 15 2021 at 23:03)</a>:</h4>
<p>But that does point to a thing: anyone interpreting LLVM bitcode emitted by Rust <em>mostly</em> needs to worry about known <code>link_llvm_intrinsics</code>.</p>



<a name="238931643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931643">(May 15 2021 at 23:03)</a>:</h4>
<p>which, effectively, we have lists of, since we have them listed in <code>core::arch</code>.</p>



<a name="238931820"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238931820" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238931820">(May 15 2021 at 23:06)</a>:</h4>
<p><span class="user-mention" data-user-id="281757">@Jubilee</span> The way we work is:</p>
<ol>
<li>Use RUSTFLAGS to make cargo compile code with LTO enabled and emitting LLVM-IR.</li>
<li>Grovel around in the target directory to find the resulting .bc file </li>
<li>Postprocess the .bc file using a tool based on the Inkwell LLVM-IR crate. Postprocessing substitutes emulation functions for SIMD intrinsics, replaces GNU-libc initializer section magic with code, and &lt;something else I forget&gt;.</li>
<li>Run KLEE on the postprocessed file.</li>
</ol>
<p>Along the way, assembly code containing actual x86 instructions is generated - but only because there is no obvious way to disable it.</p>
<p>(Actually, we do use the x86 binary for one purpose: we want to emulate 'cargo test' which requires us to get a list of all the #[test] functions. We do this by running the output of 'cargo test' with a flag that makes it print out the names of all the tests. Then we mangle the names and use the mangled names as the names of entrypoints for KLEE. Alas, this disgusting hack stopped working with more recent rustc versions...)</p>



<a name="238932130"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238932130" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238932130">(May 15 2021 at 23:12)</a>:</h4>
<p><span class="user-mention" data-user-id="312331">@Caleb Zulawski</span> I'm not sure if you <em>need</em> to emulate the LLVM intrinsics. But one reason that you might want to (even if using cranelift) is that, at the moment, some of the x86 intrinsics are implemented as ordinary functions which then call the LLVM intrinsic. e.g., vector add, sub, mul, and other simple/obvious/portable instructions are handled this way.</p>
<p>Of course, the introduction of cranelift might result in a layer of indirection being introduced so that the path is<br>
x86-intrinsic --&gt; Rust intrinsic --&gt; {cranelift intrinsic, LLVM intrinsic}.<br>
But, still ends up with the need for emulation of the second or final step in that path.</p>



<a name="238932872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238932872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238932872">(May 15 2021 at 23:26)</a>:</h4>
<p>btw Although I am working at the LLVM level and only need to cope with things that LLVM cannot lower for me, I think the approach I am taking would also work for MIR-based tools like miri, for formal verification tools like Crux-MIR, MIRAI, RMC, Prusti, and, I think, CTFE, portable SIMD, etc.<br>
I am very keen that the library should support these other users because I think it would be crazy if every formal verification tool had its own independent solution to the problem - resulting in duplicated work, highly variable levels of testing (at present, my crate is basically untested), incomplete coverage, etc.<br>
Probably requires some compromises to make it useful to a wide range of different uses - but well worth doing.</p>
<p>(I think this is basically the only way that large artifacts like this can be created/maintained/etc. - I did something very similar when I created Arm's formal ISA specification - making sure that there were lots of different uses within Arm for an executable specification.)</p>



<a name="238933200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238933200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238933200">(May 15 2021 at 23:32)</a>:</h4>
<p><span class="user-mention silent" data-user-id="336739">Alastair Reid</span> <a href="#narrow/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification/near/238931820">said</a>:</p>
<blockquote>
<p>Along the way, assembly code containing actual x86 instructions is generated - but only because there is no obvious way to disable it.</p>
</blockquote>
<p>Hmm, do you know at what step x86 assembly is generated? Is it before Inkwell or after?</p>



<a name="238933820"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238933820" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jubilee <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238933820">(May 15 2021 at 23:44)</a>:</h4>
<blockquote>
<p>at the moment, some of the x86 intrinsics are implemented as ordinary functions which then call the LLVM intrinsic. e.g., vector add, sub, mul, and other simple/obvious/portable instructions are handled this way.</p>
</blockquote>
<p>Yeah, what we do internally at the moment is we call a rustc "platform function" that has to be implemented by any target which wants to compile Rust. One of the things we hope to do is implement a way that these functions can be understood in a portable manner internally and lowered to scalar code if necessary.</p>
<blockquote>
<p>Of course, the introduction of cranelift might result in a layer of indirection being introduced so that the path is<br>
x86-intrinsic --&gt; Rust intrinsic --&gt; {cranelift intrinsic, LLVM intrinsic}.<br>
But, still ends up with the need for emulation of the second or final step in that path.</p>
</blockquote>
<p>That actually exists internally already: there is a <code>rustc_codegen_ssa</code> crate that describes an abstraction shared by the codegen backends, so that they mostly describe the specifics of their individual lowerings.</p>



<a name="238936193"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/257879-project-portable-simd/topic/Emulation%20of%20SIMD%20for%20verification/near/238936193" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/257879-project-portable-simd/topic/Emulation.20of.20SIMD.20for.20verification.html#238936193">(May 16 2021 at 00:31)</a>:</h4>
<blockquote>
<p>Hmm, do you know at what step x86 assembly is generated? Is it before Inkwell or after?</p>
</blockquote>
<p>rustc generates LLVM IR and saves it somewhere in the target directory. LLVM then uses the LLVM IR to generate assembly. Once cargo is all done (i.e. has generated an x86 binary), we grab the LLVM IR and run our postprocessor tool.  Our postprocessor uses the Inkwell crate to read and write LLVM IR from a file. In the middle of that process [edit: i.e., the postprocessing process], we scan for x86 intrinsics for which we have an emulation function and replace them.<br>
So, if you drew a dataflow graph, it is a Y-shaped graph where one fork leads to x86 assembly (that we basically ignore) and the other fork leads to LLVM IR that we postprocess to patch up the x86-specific intrinsics in.<br>
(Note that, instead of using a postprocessor, we could have patched KLEE to perform the substitution as it executes each instruction. This would probably be the right choice for miri, for example.)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>